cr-fails-before(es; Sys; chain; x; y) == e:E(Sys). ((y  chain(e)) & ((x  chain(e)))) 

latex

---

clarification:

cr-fails-before(es; Sys; chain; x; y)
== e:es-E-interface(es;Sys). ((y  chain(e)  Id) & ((x  chain(e)  Id))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	cr-fails-before wf
Definitions	x:A. B(x), E(X), P & Q, A, (x  l), f(a), Id
FDL editor aliases	cr-fails-before